Nuprl Definition : es-bact 0,22

action[[a n]][e1;e2]
== Case TERMOF{decidable ecl-es-act:ObjectId, 1:l, i:l}(ds,da,a,es,loc(e1),x.*,x,y*,n,e1,e2) of
== inl(x true
== inr(x false 
latex



clarification:

es-bact{i:l}
es-bact(dsdaaesne1e2)
== Case TERMOF{decidable ecl-es-act:ObjectId, 1:l, i:l}
== Case (ds
== Case ,da
== Case ,a
== Case ,es
== Case ,es-loc(ese1)
== Case ,x.*
== Case ,x,y*
== Case ,n
== Case ,e1
== Case ,e2) of
== inl(x true
== inr(x false 
latex


Definitionsaction[[a n]][e1;e2], decidable ecl-es-act, loc(e), true, false
FDL editor aliaseses-bact

origin